T:Type, P:(TProp), L, L':T List. (xL. P(x))  L = L'  L = L'  {x:T| P(x) } List 

latex

Definitions	l[i], <a,b>, ||as||, t  T, f(a), x.A(x), P  Q, x. t(x), x:A. B(x), , {x:A| B(x) }, x:AB(x), a<b, Prop, s = t, False, A, AB, , type List, S  T, Type, x(s), xL. P(x), #$n, Void, (x  l), x:AB(x), P & Q, i  j < k, {i..j}
Lemmas	select member, le wf, select wf, l all wf, list extensionality, length wf1, nat wf, list-set-type2